

Checking transition consistency


msc diagrams: three_way_teardown1(5) and three_way_teardown2(2)
INCONSISTENCY:
Matching formula: m5 = k2
Precondition 1: rel (m5 , n5 , three_wayconnected k5); Precondition 2: rel (m2 , n2 , three_wayconnected k2);
Post condition 1: rel (n5 , k5 , connected); Post condition 2: state (m2 , dial) & state (n2 , dial);